; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((Nat!2409 0)) (((succ!2410 (pred!2411 Nat!2409)) (zero!2412))
))
(declare-datatypes ((Lst!2413 0)) (((cons!2414 (head!2415 Nat!2409) (tail!2416 Lst!2413)) (nil!2417))
))
(declare-fun error_value!2418 () Nat!2409)
(declare-fun plus!237 (Nat!2409 Nat!2409) Nat!2409)
(declare-fun error_value!2419 () Nat!2409)
(declare-fun count!263 (Nat!2409 Lst!2413) Nat!2409)
(declare-fun pred!2411_uf_1 (Nat!2409) Nat!2409)
(declare-fun tail!2416_uf_2 (Lst!2413) Lst!2413)
(declare-fun head!2415_uf_3 (Lst!2413) Nat!2409)
(declare-sort I_plus!237 0)
(set-info :notes "plus!237_arg_0_4 is op created during fun def fmf")
(declare-fun plus!237_arg_0_4 (I_plus!237) Nat!2409)
(set-info :notes "plus!237_arg_1_5 is op created during fun def fmf")
(declare-fun plus!237_arg_1_5 (I_plus!237) Nat!2409)
(declare-sort I_count!263 0)
(set-info :notes "count!263_arg_0_6 is op created during fun def fmf")
(declare-fun count!263_arg_0_6 (I_count!263) Nat!2409)
(set-info :notes "count!263_arg_1_7 is op created during fun def fmf")
(declare-fun count!263_arg_1_7 (I_count!263) Lst!2413)
(assert
(and
(not (forall ((h!413 Nat!2409) (BOUND_VARIABLE_663 I_plus!237) (BOUND_VARIABLE_671 I_count!263) (BOUND_VARIABLE_679 I_count!263) (BOUND_VARIABLE_687 I_count!263) (BOUND_VARIABLE_695 I_plus!237) (BOUND_VARIABLE_703 I_count!263) (BOUND_VARIABLE_711 I_count!263) (BOUND_VARIABLE_719 I_count!263)) (or (not (= (plus!237 (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) (= (plus!237 (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679))) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_663) (count!263 (count!263_arg_0_6 BOUND_VARIABLE_671) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_671) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_679) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_687) (count!263_arg_0_6 BOUND_VARIABLE_671))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_687) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (plus!237_arg_0_4 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (cons!2414 h!413 nil!2417)))) (not (= (plus!237_arg_1_5 BOUND_VARIABLE_695) (count!263 (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)) (count!263_arg_1_7 BOUND_VARIABLE_679)))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_703) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_703) (cons!2414 h!413 nil!2417))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_711) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_711) (count!263_arg_1_7 BOUND_VARIABLE_679))) (not (= (count!263_arg_0_6 BOUND_VARIABLE_719) (succ!2410 (count!263_arg_0_6 BOUND_VARIABLE_671)))) (not (= (count!263_arg_1_7 BOUND_VARIABLE_719) (cons!2414 h!413 (count!263_arg_1_7 BOUND_VARIABLE_679))))) ))
(forall ((?j I_plus!237)) (= (plus!237 (plus!237_arg_0_4 ?j) (plus!237_arg_1_5 ?j)) (ite ((_ is zero!2412) (plus!237_arg_0_4 ?j)) (plus!237_arg_1_5 ?j) (ite ((_ is succ!2410) (plus!237_arg_0_4 ?j)) (succ!2410 (plus!237 (ite ((_ is succ!2410) (plus!237_arg_0_4 ?j)) (pred!2411 (plus!237_arg_0_4 ?j)) (pred!2411_uf_1 (plus!237_arg_0_4 ?j))) (plus!237_arg_1_5 ?j))) error_value!2418))) )
(forall ((?i I_plus!237)) (ite ((_ is zero!2412) (plus!237_arg_0_4 ?i)) true (ite ((_ is succ!2410) (plus!237_arg_0_4 ?i)) (not (forall ((?z I_plus!237)) (or (not (= (plus!237_arg_0_4 ?z) (ite ((_ is succ!2410) (plus!237_arg_0_4 ?i)) (pred!2411 (plus!237_arg_0_4 ?i)) (pred!2411_uf_1 (plus!237_arg_0_4 ?i))))) (not (= (plus!237_arg_1_5 ?z) (plus!237_arg_1_5 ?i)))) )) true)) )
(forall ((?i I_count!263)) (= (count!263 (count!263_arg_0_6 ?i) (count!263_arg_1_7 ?i)) (ite ((_ is nil!2417) (count!263_arg_1_7 ?i)) zero!2412 (ite ((_ is cons!2414) (count!263_arg_1_7 ?i)) (ite (= (count!263_arg_0_6 ?i) (ite ((_ is cons!2414) (count!263_arg_1_7 ?i)) (head!2415 (count!263_arg_1_7 ?i)) (head!2415_uf_3 (count!263_arg_1_7 ?i)))) (succ!2410 (count!263 (count!263_arg_0_6 ?i) (ite ((_ is cons!2414) (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) (count!263 (count!263_arg_0_6 ?i) (ite ((_ is cons!2414) (count!263_arg_1_7 ?i)) (tail!2416 (count!263_arg_1_7 ?i)) (tail!2416_uf_2 (count!263_arg_1_7 ?i))))) error_value!2419))) )
(forall ((?j I_count!263)) (ite ((_ is nil!2417) (count!263_arg_1_7 ?j)) true (ite ((_ is cons!2414) (count!263_arg_1_7 ?j)) (ite (= (count!263_arg_0_6 ?j) (ite ((_ is cons!2414) (count!263_arg_1_7 ?j)) (head!2415 (count!263_arg_1_7 ?j)) (head!2415_uf_3 (count!263_arg_1_7 ?j)))) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite ((_ is cons!2414) (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) )) (not (forall ((?z I_count!263)) (or (not (= (count!263_arg_0_6 ?z) (count!263_arg_0_6 ?j))) (not (= (count!263_arg_1_7 ?z) (ite ((_ is cons!2414) (count!263_arg_1_7 ?j)) (tail!2416 (count!263_arg_1_7 ?j)) (tail!2416_uf_2 (count!263_arg_1_7 ?j)))))) ))) true)) )
)
)
(check-sat)
